\functions {
  int div_0; int div_1;
}

\problem {
(! (! \forall int x5, x4, x3, x2, x1, x0; (! (x0 + -1*x5 + 65536*div_0 + 1 = 0 & 3*x1 + x4 + -1*x5 = 0 & x2 + -3*div_1 + -1 = 0 & 3*x3 + -1*x5 + 3*div_1 + 65536*div_0 + 2 = 0 & -1*x0 + 32767 >= 0 & x0 + 32768 >= 0 & -1*x2 + 2 >= 0 & x2 >= 0 & -1*x4 + 2 >= 0 & x4 >= 0 & -1*x5 + 32767 >= 0 & x5 + 32768 >= 0)) & ! (div_1 = 0 & div_0 + 1 = 0) & ! (div_1 = 0 & div_0 = 0)))
}